Skip to content

Add annotation support for trait methods and verify that implementations satisfy them#25

Merged
coeff-aij merged 6 commits into
coord-e:mainfrom
coeff-aij:annot-preds-trait
Feb 10, 2026
Merged

Add annotation support for trait methods and verify that implementations satisfy them#25
coeff-aij merged 6 commits into
coord-e:mainfrom
coeff-aij:annot-preds-trait

Conversation

@coeff-aij

@coeff-aij coeff-aij commented Feb 1, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

This feature allows users to annotate trait methods with predicates. The Thrust verifies that the concrete implementations of those methods and their associated predicates satisfy the annotations given in trait.

  • Example
    The specification for A::double() is expressed through the annotations on Double::double().
    The method refers to the predicate Double::is_double()(written as Self::is_double() in code), whose concrete implementation is provided by A::is_double().
// A is represented as Tuple<Int> in SMT-LIB2 format.
struct A {
    x: i64,
}

trait Double {
    // Support annotations in trait definitions
    #[thrust::predicate]
    fn is_double(self, doubled: Self) -> bool;

    // This annotations are applied to all implementors of the `Double` trait.
    #[thrust::requires(true)]
    #[thrust::ensures(Self::is_double(*self, ^self))]
    fn double(&mut self);
}

impl Double for A {
    // Write concrete definitions for predicates in `impl` blocks
    #[thrust::predicate]
    fn is_double(self, doubled: Self) -> bool {
        // (tuple_proj<Int>.0 self) is equivalent to self.x
        // self.x * 2 == doubled.x is written as following:
        "(=
            (* (tuple_proj<Int>.0 self) 2)
            (tuple_proj<Int>.0 doubled)
        )"; true
    }

    // Check if this method complies with annotations in
    // trait definition.
    fn double(&mut self) {
        self.x += self.x;
    }
}

coeff-aij
coeff-aij commented Feb 1, 2026
View reviewed changes
Comment thread src/analyze/local_def.rs Outdated
Comment on lines +287 to +290
if let Some(trait_item_id) = self.get_trait_item(){
tracing::info!("trait item fonud: {}", self.tcx.item_name(trait_item_id.into()).to_string());
let trait_require_annot = self.extract_require_annot(trait_item_id.into(), &param_resolver);
let trait_ensure_annot = self.extract_ensure_annot(trait_item_id.into(), &result_param_resolver);

@coeff-aij coeff-aij Feb 1, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can't create new instance of Analyzer for method definitions in trait because they don't appear in MIR. I have extended the self.extract_*_annot() so that they can analyze any definitions not only the one identified by self.local_def_id. This implementation works, but it could be refactored for a clearer architecture.

@coord-e coord-e Feb 2, 2026

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have extended the self.extract_*_annot() so that they can analyze any definitions not only the one identified by self.local_def_id. This implementation works, but it could be refactored for a clearer architecture.

Cool, could you move these extract_*_annot() functions that take DefId to analyze::Analyzer? I'm putting utilities that need tcx and aren't bound to crates, local defs, or basic blocks into analyze::Analyzer.

@coeff-aij coeff-aij requested a review from coord-e February 1, 2026 14:36
@coeff-aij coeff-aij marked this pull request as ready for review February 1, 2026 14:37
@coeff-aij

coeff-aij commented Feb 1, 2026

Copy link
Copy Markdown
Collaborator Author

We also need to verify that every predicate implementation defined in a trait is annotated with the #[thrust::predicate] attribute. (But I will postpone the implementation of this check for now.)

coord-e
coord-e reviewed Feb 2, 2026
View reviewed changes
Comment thread src/analyze/local_def.rs Outdated
coord-e
coord-e reviewed Feb 2, 2026
View reviewed changes
Comment thread src/analyze/local_def.rs Outdated
coeff-aij and others added 2 commits February 3, 2026 15:29
@coeff-aij
add: tests for annotations in traits
4c67ff5
@coeff-aij @coord-e
add: reference trait-side definitions for require/ensure annotations of
87d818c 
functions in impl blocks

Update src/analyze/local_def.rs

Co-authored-by: Hiromi Ogawa <me@coord-e.com>
@coeff-aij

coeff-aij commented Feb 3, 2026

Copy link
Copy Markdown
Collaborator Author

I've addressed your review comments.

coord-e
coord-e approved these changes Feb 3, 2026
View reviewed changes

@coord-e coord-e left a comment

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

thank you!

coeff-aij
coeff-aij commented Feb 7, 2026
View reviewed changes
Comment thread src/annot.rs
}

let func_name = path.segments.get(1).unwrap().ident.name.as_str();
let pred_name = if let Some(self_type_name) = &self.self_type_name {

@coeff-aij coeff-aij Feb 7, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I added a self_type_name field so that the parser can replace the concrete struct name with Self::.
However, this change forces all parsing-related structs and functions to carry self_type_name and seems to be bad idea.

@coeff-aij coeff-aij requested a review from coord-e February 7, 2026 09:06
@coeff-aij coeff-aij merged commit ff27c71 into coord-e:main Feb 10, 2026
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@coord-e coord-e coord-e approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@coeff-aij @coord-e